Cardinality constraints arise naturally in many application fields, such as artificial intelligence, operational research, formal verification, combinatorial optimization, constraint programming, error localization and more. One ubiquitous example is encoding of multi-valued variables into propositional form: given a multi-valued variable V with possible domain values V1, . . . , Vn, usually one introduces auxiliary Boolean (indicator) variables b1, . . . , bn, so that each bk is true if and only if (V=Vk), and one adds the “exactly one” constraint on the variables b1, . . . , bn (to enforce V taking exactly one value). Such constraints are natural for example in the translation of constraint satisfaction problems into SAT problems.
A Boolean formula may be represented in Conjunctive Normal Form (CNF). A formula is said to be in CNF if it is a conjunction of clauses, where a clause is a disjunction of literals.
CNF encodings are often used for modern Boolean Satisfiability Problem (SAT) solvers for finding solutions to the more general problems. The state-of-the-art SAT solvers have been highly optimized over the years, and they perform quite well on many CNF formulas arising from practical problems. Their runtime, however, is still (generally) quite sensitive to the number of variables and clauses in the given formula.